ds, da, T:Top, ks:Top List, upd:x:KndId fp Top, a:Top, i, j:Id.
R-has-loc(ecl-machine2(i;ds;da;"ecl";T;ks;a;upd);j) ~ (null(update-spec-vars(upd))  i = j) 

latex

Definitions	t  T, Void, x:A. B(x), Id, Knd, x:AB(x), x:A. B(x), fpf-domain(f), x:AB(x), x. t(x), 2of(t), x.A(x), map(f;as), P  Q, ecl-machine2(i;ds;da;x;T;ks;a;upd), a:A fp B(a), update-spec-vars(upd), Top, type List, s = t, false, , reduce(f;k;as), <a,b>, true, p  q, Prop, b, Type, A, b, P & Q, P  Q, Unit, left+right, {T}, SQType(T), s ~ t, a = b
Lemmas	bool sq, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-eq-id, bnot wf, not wf, assert wf, eq id wf, bool wf, btrue wf, bfalse wf, fpf wf, Rall-has-loc, R-state-var-loc, map wf, pi2 wf, fpf-domain wf, Knd wf, Id wf, top wf